\section{Árbol de Categorías}

\begin{Interfaz}
  
% 	\textbf{parámetros formales}\hangindent=2\parindent\\
% 	\parbox{1.7cm}{\textbf{géneros}} 

	\textbf{se explica con}: \tadNombre{ÁrbolCategorías}, \tadNombre{Iterador Unidereccional(nodoItAc)}

	\begin{Tupla}[nodoItAc]
		\tupItem{cat}{string}
		\tupItem{id}{nat}
		\tupItem{tienePadre}{bool}
		\tupItem{padre}{string}
		\tupItem{padreId}{nat}
	\end{Tupla}

	\textbf{géneros}: \TipoVariable{acat}, \TipoVariable{itAcat}
	
	\Titulo{operaciones del árbol de categorías}

	\InterfazFuncion{Nuevo}{\In{raiz}{string}}{acat}%
	[$\neg$vacía($\somb{raiz}$)]
	{$\somb{res} \igobs $ nuevo($\somb{raiz}$)}
	[$\Theta(|raiz|)$]
	[Genera un arbol de categorías con la categoría $raiz$ como raíz del árbol.]

	\InterfazFuncion{Agregar}{\Inout{ac}{acat}, \In{padre}{string}, \In{hija}{string}}{}
	[$\somb{ac} \igobs ac_0$ $\land$ está?($\somb{padre},\somb{ac}$) $\land$ $\neg$vacía?($\somb{hija}$) $\land$ $\neg$está?($\somb{hija},\somb{ac}$)]
	{$\somb{ac} \igobs \textrm{agregar}(ac_0, \somb{padre}, \somb{hija})$} % NOTE: No va un alias porque copia los parámetros. --eze
	[$\Theta(|padre| + |hija|)$]
	[Agrega la categoría $hija$ al árbol $ac$ con $padre$ como categoría padre.]
	
	\InterfazFuncion{Raiz}{\In{ac}{acat}}{string}
	{$\somb{res} \igobs \textrm{raíz}(\somb{ac})$ $\land$ alias($\somb{res}$ $\igobs$ raiz($\somb{ac}$))}
	[$\Theta(1)$] %FIXME: ¿Y si la devuelve por copia? --eze
	[Devuelve la categoría raíz del árbol de categorías $ac$.]
	
	\InterfazFuncion{Padre}{\In{ac}{acat}, \In{hija}{string}}{string}
	[está?($\somb{hija}$, $\somb{ac}$) $\land$ $\neg$(raíz($\somb{ac}$) = $\somb{hija}$)]
	{$\somb{res} \igobs \textrm{padre}(\somb{hija}, \somb{ac})$  $\land$ alias($\somb{res}$ $\igobs$ padre($\somb{hija}, \somb{ac}$))}
	[$\Theta(|hija|)$] %FIXME: ¿Y si la devuelve por copia? --eze
	[Devuelve el padre de la cateogoría $hija$ dentro del árbol $ac$.]
	
	\InterfazFuncion{Id}{\In{ac}{acat}, \In{cat}{string}}{nat}
	[está?($\somb{cat}$, $\somb{ac}$)]
	{$\somb{res} \igobs \textrm{id}(\somb{cat}, \somb{ac})$}
	[$\Theta(|cat|)$]
	[Devuelve el Id de la categoría $cat$ dentro del árbol $ac$.]

	\InterfazFuncion{CantCategorias}{\In{ac}{acat}}{nat}
	{$\somb{res} \igobs \#categorias(\somb{ac})$}
	[$\Theta(1)$]
	[Devuelve la cantidad de categorías en el árbol]
	
	\Titulo{Operaciones del iterador itAcat}

	\InterfazFuncion{CrearIt}{\In{ac}{acat}, \In{padre}{string}}{itAcat}
	{alias(esPermutación(SecuSuby($\somb{res}$), ConstruirHijosIt($\somb{ac}$, $\somb{p}$))) $\land$ vacia?(Anteriores($\somb{res}$))}
	[$\Theta(|padre|)$]
	[Crea un iterador unidireccional de los hijos de la categoría $padre$ en el árbol $ac$.]

	\InterfazFuncion{CrearItHijosRaiz}{\In{ac}{acat}}{itAcat}
	{alias(esPermutación(SecuSuby($\somb{res}$), ConstruirHijosIt($\somb{ac}$, raíz($\somb{ac}$))) $\land$ vacía?(Anteriores($\somb{res}$))}
	[$\Theta(1)$]
	[Crea un iterador unidireccional de los hijos de la raíz en el árbol $ac$]

	\InterfazFuncion{CrearItHijosIt}{\In{ac}{acat}, \In{it}{itAcat}}{itAcat}
	{HayMas?($\somb{it}$) \yluego alias(esPermutación(SecuSuby($\somb{res}$), \\
	ConstruirHijosIt($\somb{ac}$, Siguiente($\somb{it}$).cat))) $\land$ vacía?(Anteriores($\somb{res}$))}
	[$\Theta(1)$]
	[Crea un iterador unidireccional de los hijos de Siguiente(it) en el árbol $ac$]
	
	\InterfazFuncion{HayMas}{\In{it}{itAcat}}{bool}
	{$\somb{res}$ $\igobs$ HayMas?($\somb{it}$)}
	[$\Theta(1)$]
	[Devuelve true sí y sólo sí en el iterador $it$ quedan elementos para avanzar.]
	
	\InterfazFuncion{Siguiente}{\In{it}{itAcat}}{nodoItAc}
	[HayMas?($\somb{it}$)]
	{alias($\somb{res}$ $\igobs$ Actual($it$))}
	[$\Theta(1)$]
	[Devuelve el elemento actual del iterador $it$.]

	\InterfazFuncion{Avanzar}{\Inout{it}{itAcat}}{}
	[HayMas?($\somb{it}$) $\land$ $\somb{it}$ $\igobs$ $it_0$]
	{$\somb{it}$ $\igobs$ Avanzar($it_0$)}
	[$\Theta(1)$]
	[Avanza al siguiente elemento en el iterador $it$.]

\end{Interfaz}

\begin{Representacion}
	\Titulo{Representación del árbol de categorías}

	\begin{Estructura}{acat}[estr]
		\begin{Tupla}[estr]
			\tupItem{raiz}{puntero(nodo)}%
			\tupItem{ultimoId}{nat}%
			\tupItem{categorias}{dicctrie(puntero(nodo))}%FIXME: Revisar TODA la implementación, Rep y Abs.
		\end{Tupla}

		\begin{Tupla}[nodo]
			\tupItem{id}{nat}%
			\tupItem{cat}{string}%
			\tupItem{padre}{puntero(nodo)}%
			\tupItem{hijos}{lista(puntero(nodo))}%
		\end{Tupla}
	\end{Estructura}

	
% 	Invariante en castellano:
% 		- El campo raíz tiene que ser igual al único nodo sin padre del diccionario categorías.
%		- Tiene que haber un único nodo sin padre en el diccionario categorías (la raíz).
%		- últimoID tiene que ser igual al tamaño del diccionario categorías.
% 		- Los ids de todos los nodos deben ser únicos, correlativos, entre 1 y ultimoId y la raíz tiene que tener id = 1.
%		- Para cada cateogoría en categorías, los hijos tienen que ser categorías dentro del diccionario categorías y
% 		  tienen que tener como padre a esa categoría.
%		- No pueden haber categorías repetidas en los hijos de una categoría.
%		- No sé si es necesario, pero el campo cat del nodo tiene que ser igual a la categoría clave que hace referencia
%		  a ese nodo.
% 		- No tiene que haber categorías vacías ni repetidas.
%		- No tienen que haber circuitos en el árbol

\Subtitulo{invariante en castellano}

\begin{enumerate}
	\item Tiene que tener al menos una categoría (la raíz).
	\item Tiene que haber un único nodo sin padre en el diccionario $categor\acute{i}as$ (la raíz).
	\item $ra\acute{i}z$ tiene que ser igual al único nodo sin padre del diccionario $categor\acute{í}as$.
	\item $\acute{u}ltimoId$ tiene que ser igual al tamaño del diccionario categorías.
	\item Los ids de todos los nodos deben ser únicos, correlativos, entre 1 y ultimoId y la raíz tiene que tener id = 1.
	\item No pueden haber categorías ``vacías''.
	\item El campo $cat$ de cada nodo tiene que ser igual a la categoría clave que hace referencia a él.
	\item Para cada categoría en $categor\acute{i}as$, los hijos tienen que ser categorías dentro del diccionario $categor\acute{i}as$ y
		   tienen que tener como padre a esa $categor\acute{i}a$.
	\item No pueden haber categorías repetidas en los hijos de una categoría.
	\item No tienen que haber circuitos en el árbol.
\end{enumerate}

\Subtitulo{invariante}

\Rep[$\somb{estr}$][e]{
	((\#(claves($e$.categorias)) > 0) \\
	\yluego (\existe{cateogría}{c})($c$ $\in$ claves($e$.categorias) \yluego EsRaíz($c$, $e$.categorias) $\land$ obtener($c$, $e$.categorias) = $e$.raiz)) \\
	$\land$ ($e$.ultimoId = \#(claves($e$.categorias))) \\
	$\land$ ((\paratodo{categoría}{c})($c$ $\in$ claves($e$.categorias)) \impluego (obtener($c$, $e$.categorias)\DRef id $\geq$ 1 $\land$ obtener($c$, $e$.categorias)\DRef id $\leq$ $e$.ultimoId)) \\
	$\land$ ($e$.raiz\DRef id \igobs 1) \\
	$\land$ ((\paratodo{categoría}{c})($c$ $\in$ claves($e$.categorias)) \impluego ($c$ $\neq$ '')) \\
	$\land$ ((\paratodo{categoría}{c})($c$ $\in$ claves($e$.categorias)) \impluego ($c$ \igobs obtener($c$, $e$.categorias)\DRef cat)) \\
	$\land$ ((\paratodo{categoría}{c})($c$ $\in$ claves($e$.categorias)) \impluego ((\paratodo{categoría}{c'})(($c'$ $\in$ *(obtener($c$, $e$.categorias)).hijos) \impluego ($c'$ $\in$ claves($c$, $e$.cateogorías) \yluego obtener($c'$, $e$.categorias)\DRef padre = $c$)))) \\
	$\land$ ((\paratodo{categoría}{c})($c$ $\in$ claves($e$.categorias)) \impluego Únicos(obtener($c$, $e$.categorias)\DRef hijos)) \\
	$\land$ NoTieneCiclos($e$.raiz))
}
	
	\vspace{15pt}
	~
	
	\tadOperacion{EsRaíz}{categoría/c, dicc(categoría nodo)/cs}{bool}{($c$ $\in$ claves($cs$)}
	\tadAxioma{EsRaíz($c$, $cs$)}{obtener($c$, $cs$)\DRef padre \igobs NULL $\land$ (\paratodo{categoría}{c'})(($c'$ $\in$ claves($cs$) \yluego obtener($c'$, $cs$))\DRef padre = NULL) \impluego $c'$ \igobs $c$)}

	~
	
	\tadOperacion{NoTieneCiclos}{puntero(nodo)/p}{bool}{$\neg$($p$ \igobs NULL)}
	\tadAxioma{NoTieneCiclos($p$)}{NoTieneCiclosAux($p\; \puntito <>$,$<>$)}

	~
	
	\tadOperacion{NoTieneCiclosAux}{secu(puntero(nodo)),secu(puntero(nodo))}{bool}{}
	\tadAxioma{NoTieneCiclosAux($avisitar$,$visitados$)}{
		vacía?($avisitar$) \oluego $\neg$(está?(prim($avisitar$),$visitados$)) \yluego
		NoTieneCiclosAux( prim($avisitar$)\DRef hijos \& fin($avisitar$), prim($avisitar$) \puntito $visitados$ )
	}
	
	~
	
	\tadOperacion{Únicos}{secu($\alpha$))}{bool}{}
	\tadAxioma{Unicos($s$)}{$\neg$(está?(prim($s$),fin($s$))) \yluego Unicos(fin($s$))}
	
	~
	
	\Subtitulo{función de abstracción}
	
	\Abs[$\somb{estr}$]{acat}[e]{ac}{
		(raíz(ac) \igobs $e$.raiz $\land$ ((\paratodo{categoría}{c})((c $\in$ categorias(ac)) \ssi def?($c$, $e$.categorias)) \yluego ($c$ $\in$ categorias($ac$)) \impluego ((padre($c$, $ac$) \igobs obtener($c$, $e$.categorias)\DRef padre\DRef cat) $\land$ (id($c$, $ac$) \igobs obtener($c$, $e$.categorias)\DRef id)))
	}
	
	~
	
	\Titulo{Representación del iterador}

	~

	\begin{Estructura}{itAcat}[itLista(puntero(nodo))]
	\end{Estructura}

	~
	
	\Rep[$\somb{itLista(puntero(nodo))}$][e]{$\neg$ está?(NULL,SecuSuby($e$))}

	~
	
	\Abs[$\somb{itLista(puntero(nodo))}$]{itUni(nodoItAc)}[e]{it}{
		Siguientes($it$) $\igobs$ ConstruirSecu(Siguientes($e$))
	}

	~

	\tadOperacion{ConstruirSecu}{secu(puntero(nodo))/s}{secu(nodoItAc)}{$\neg$ está?(NULL,$s$)}
	\tadAxioma{ConstruirSecu($s$)}{
		\IF vacía?($s$) THEN $<>$ ELSE {
			\IF (*prim($s$)).padre = NULL THEN
				$\langle$(*prim($s$)).cat, (*prim($s$)).id, \textbf{false}, ``'', 0$\rangle$
			ELSE
				$\langle$(*prim($s$)).cat, (*prim($s$)).id, \textbf{true}, (*((*prim($s$)).padre)).cat, (*((*prim($s$)).padre)).id$\rangle$
			FI
			\puntito ConstruirSecu(fin($s$))
		}
		FI
	}

	~

	\tadOperacion{ConstruirHijosIt}{acat/ac, categoría/c}{secu(nodoItAc)}{está?($c$,$ac$)}
	\tadAxioma{ConstruirHijosIt($ac$,$c$)}{ConstruirSecuencia(ac,hijos(ac,c))}

	~

	\tadOperacion{ConstruirSecuencia}{acat, conj(categoría)}{secu(nodoItAc)}{}
	\tadAxioma{ConstruirSecuencia($ac$,$cs$)}{
		\IF $\emptyset?(cs)$ THEN $\emptyset$ ELSE {
			\IF dameUno($cs$) = raíz($ac$) THEN
				Ag( $\langle$dameUno($cs$), id($ac$,dameUno($cs$)), \textbf{false}, ``'', 0$\rangle$, ConstruirSecuencia(sinUno($cs$)) )
			ELSE
				Ag( $\langle$dameUno($cs$), id($ac$,dameUno($cs$)), \textbf{true}, padre($ac$,dameUno($cs$)), id(padre($ac$,dameUno($cs$)))$\rangle$, ConstruirSecuencia(sinUno($cs$)) )
			FI
		}
		FI
	}

\end{Representacion}

\begin{Algoritmos}
	
	\Titulo{Algoritmos del árbol de categorías}
	
	~
	
	\Implementacion{iNuevo}{\In{r}{string}}{estr}
	\begin{algorithmic}
		\State var raiz : puntero(nodo)
		\State var categorias : dicctrie
		\State raiz \asignar CrearNodo(1, r, NULL)
		\State categorias \asignar Vacío()
		\State categorias \asignar Definir(categorias, r, raiz)
		\State \res.raiz \asignar raiz
		\State \res.ultimoId \asignar 1
		\State \res.categorias \asignar categorías
	\end{algorithmic}

	~

	\Implementacion{iAgregar}{\Inout{ac}{estr}, \In{padre}{string}, \In{hija}{string}}{}
	\begin{algorithmic}
		\State var nodoPadre, nuevoNodo : puntero(nodo)
		\State ac.ultimoId \asignar ac.ultimoId + 1
		\State nodoPadre \asignar Obtener(ac.categorias, padre)
		\State nuevoNodo \asignar CrearNodo(ac.ultimoId, hija, nodoPadre)
		\State AgregarAtrás((*nodoPadre).hijos, nuevoNodo)
		\State Definir(ac.categorias, hija, nuevoNodo)
	\end{algorithmic}

	~

	\Implementacion{iRaiz}{\In{ac}{estr}}{string}
	\begin{algorithmic}
		\State \res \asignar (*ac.raiz).cat
	\end{algorithmic}

	~

	\Implementacion{iPadre}{\In{ac}{puntero(nodo)}, \In{cat}{string}}{string}
	\begin{algorithmic}
		\State var p : puntero(nodo) \asignar Obtener(ac.categorias, cat)
		\State \res \asignar (*(*p).padre).cat
	\end{algorithmic}

	~
	
	\Implementacion{iId}{\In{ac}{puntero(nodo)}, \In{cat}{string}}{nat}
	\begin{algorithmic}
		\State var p : puntero(nodo) \asignar Obtener(ac.categorias, cat)
		\State \res \asignar (*p).id
	\end{algorithmic}

	~

	\Implementacion{iCantCategorias}{\In{ac}{estr}}{nat}
	\begin{algorithmic}
		\State \res \asignar ac.ultimoId
	\end{algorithmic}
	
	~

	\Implementacion{CrearNodo}{\In{id}{nat}, \In{cat}{string}, \In{padre}{puntero(nodo)}}{puntero(nodo)}\\
	%\textbf{Pre} $\equiv$ \{$\neg$vacía?($\somb{cat}$)\}\\
	%\textbf{Post} $\equiv$ \{(*$\somb{res}$) \igobs $\langle \somb{id}, \somb{cat}, \somb{padre}, <> \rangle$\}\\
	%\textbf{Complejidad:} $\Theta(1)$
	\begin{algorithmic}
		\State var n : nodo
		\State n.id    \asignar id
		\State n.cat   \asignar cat
		\State n.padre \asignar padre
		\State n.hijos \asignar Vacía() 
		\State \res \asignar \&n
	\end{algorithmic}

	\Titulo{Algoritmos del iterador itAcat}

	~

	\Implementacion{iCrearIt}{\In{ac}{estr}, \In{padre}{string}}{itLista(puntero(nodo))}
	\begin{algorithmic}
		\State var p : puntero(nodo)
		\State p \asignar Obtener(ac.categorias,padre)
		\State \res \asignar CrearIt((*p).hijos)
	\end{algorithmic}

	~

	\Implementacion{iCrearItHijosRaiz}{\In{ac}{estr}}{itLista(puntero(nodo))}
	\begin{algorithmic}
		\State var p : puntero(nodo) \asignar ac.raiz
		\State \res \asignar CrearIt( (*p).hijos )
	\end{algorithmic}

	~

	\Implementacion{iCrearItHijosIt}{\In{ac}{estr}, \In{it}{itLista(puntero(nodo))}}{itLista(puntero(nodo))}
	\begin{algorithmic}
		\State var p : puntero(nodo) \asignar Siguiente(it)
		\State \res \asignar CrearIt( (*p).hijos )
	\end{algorithmic}

	~

	\Implementacion{iHayMas}{\In{it}{itLista(puntero(nodo))}}{bool}
	\begin{algorithmic}
		\State \res \asignar HaySiguiente(it)
	\end{algorithmic}

	~
	
	\Implementacion{iSiguiente}{\In{it}{itLista(puntero(nodo))}}{nodoItAc}
	\begin{algorithmic}
		\State var p : puntero(nodo) \asignar Siguiente(it)
		\State var n : nodoItAc
		\State n.cat \asignar (*p).cat
		\State n.id \asignar (*p).id
		\If{(*p).padre = NULL}
			\State n.tienePadre \asignar false
		\Else
			\State n.tienePadre \asignar true
			\State n.padre \asignar (*((*p).padre)).cat
			\State n.padreId \asignar (*((*p).padre)).id
		\EndIf
		\State \res \asignar n
	\end{algorithmic}

	~

	\Implementacion{iAvanzar}{\Inout{it}{itLista(puntero(nodo))}}{}
	\begin{algorithmic}
		\State Avanzar(it)
	\end{algorithmic}

\end{Algoritmos}
